es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id }Prop).
e@loc(e'). Dec(P(e))  (e<e'.e is first@ loc(e') s.t.  e.P(e)  e<e'.P(e)) 

latex

Definitions	t  T, x:A. B(x), P  Q, ES, E, Prop, Id, x(s), Dec(P), x. t(x), e@i. P(e), loc(e)
Lemmas	alle-at wf, decidable wf, Id wf, es-E wf, event system wf, es-first-before, es-loc wf